T, A:Type, L:T List, R:(||L||||L||Prop), P, Q:(A||L||Prop).
(Trans _1,_2:||L||. R(_1,_2))
 (x:A. causal_order(L;R;i.P(x,i);i.Q(x,i)))
 causal_order(L;R;i.x:A. P(x,i);i.x:A. Q(x,i)) 

latex

Definitions	t  T, x(s1,s2), x:A. B(x), x:A. B(x), ||as||, P  Q, False, A, AB, P & Q, i  j < k, {i..j}, Prop, x,y. t(x;y), Trans x,y:T. E(x;y), causal_order(L;R;P;Q)
Lemmas	trans wf, int seg wf, length wf1, le wf